Create a new input syntax for function. #1254

DavidFangWJ · 2024-03-25T13:47:04Z

Motivation

Add a more compact syntax to function, such that

let f(x : A, y: B): C = 
  e

should behave the same as below:

let f : (A, B) -> C = 
  fun (x, y) -> e

This new function syntax is more analogous to other programming languages with strong data types, and is therefore easier to learn.

Implementation Strategy

I believe that it will mostly be a modification of Form.re.

Add new syntax expression
Make sure that its further processing is identical to existing function syntax

cyrus- · 2024-03-26T21:55:26Z

@DavidFangWJ We shouldn't actually need to modify Form.re to accomplish this, since the syntax of patterns already includes application and annotations:

We will need to change how patterns in let bindings are processed in the statics and elaboration to special case the situation where the top-level pattern is x(p1[: t1], ..., pn[: tn])[ : t].

cyrus- · 2024-04-12T01:20:37Z

Regarding the type error, take a look at the definition of UPat.t -- it is a record type, because terms have unique IDs, so you need to decompose it like the other functions working on UPat's do.

Regarding the function itself, you should be looking for the application of a variable, rather than a constructor. Constructors are capitalized.

You also do not need to check that all arguments have type annotations -- it is okay to leave an argument unannotated, it will just get the unknown type.

You also need to handle optional return type annotations (which will require changing the return type of your function overall).

Please write some additional examples in your PR message to handle both functions with missing type annotations on arguments and missing return types, so make it clear these are all valid. We'll turn these into tests as well.

src/haz3lcore/statics/Statics.re

…/hazel into haz3l-new-func-syntax

DavidFangWJ · 2024-05-08T23:50:32Z

Cannot fully understand the part in Statics.re/uexp_to_info_map regarding the process of let binding, which looks like this:

  | Let(p, def, body) =>
    let (p_syn, _) =
      go_pat(~is_synswitch=true, ~co_ctx=CoCtx.empty, ~mode=Syn, p, m);
    let (def, p_ana_ctx, m, ty_p_ana) =
      if (!is_recursive(ctx, p, def, p_syn.ty)) {
        let (def, m) = go(~mode=Ana(p_syn.ty), def, m);
        let ty_p_ana = def.ty;
        let (p_ana', _) =
          go_pat(
            ~is_synswitch=false,
            ~co_ctx=CoCtx.empty,
            ~mode=Ana(ty_p_ana),
            p,
            m,
          );
        (def, p_ana'.ctx, m, ty_p_ana);
      } else {
        let (def_base, _) =
          go'(~ctx=p_syn.ctx, ~mode=Ana(p_syn.ty), def, m);
        let ty_p_ana = def_base.ty;
        /* Analyze pattern to incorporate def type into ctx */
        let (p_ana', _) =
          go_pat(
            ~is_synswitch=false,
            ~co_ctx=CoCtx.empty,
            ~mode=Ana(ty_p_ana),
            p,
            m,
          );
        let def_ctx = p_ana'.ctx;
        let (def_base2, _) = go'(~ctx=def_ctx, ~mode=Ana(p_syn.ty), def, m);
        let ana_ty_fn = ((ty_fn1, ty_fn2), ty_p) => {
          ty_p == Typ.Unknown(SynSwitch) && !Typ.eq(ty_fn1, ty_fn2)
            ? ty_fn1 : ty_p;
        };
        let ana =
          switch ((def_base.ty, def_base2.ty), p_syn.ty) {
          | ((Prod(ty_fns1), Prod(ty_fns2)), Prod(ty_ps)) =>
            let tys =
              List.map2(ana_ty_fn, List.combine(ty_fns1, ty_fns2), ty_ps);
            Typ.Prod(tys);
          | ((ty_fn1, ty_fn2), ty_p) => ana_ty_fn((ty_fn1, ty_fn2), ty_p)
          };
        let (def, m) = go'(~ctx=def_ctx, ~mode=Ana(ana), def, m);
        (def, def_ctx, m, ty_p_ana);
      };
    let (body, m) = go'(~ctx=p_ana_ctx, ~mode, body, m);
    /* add co_ctx to pattern */
    let (p_ana, m) =
      go_pat(
        ~is_synswitch=false,
        ~co_ctx=body.co_ctx,
        ~mode=Ana(ty_p_ana),
        p,
        m,
      );
    add(
      ~self=Just(body.ty),
      ~co_ctx=
        CoCtx.union([def.co_ctx, CoCtx.mk(ctx, p_ana.ctx, body.co_ctx)]),
      m,
    );

cyrus- · 2024-08-20T17:36:00Z

@DavidFangWJ there is a small merge conflict + the following has an error on f:

… 446.

For draft PR

7280a28

cyrus- marked this pull request as draft March 27, 2024 02:57

cyrus- added the in-development for PRs that remain in development label Mar 29, 2024

Could not compile for now

1077ddc

DavidFangWJ added 2 commits April 14, 2024 17:06

Confused on how to write it.

948cbc7

Can compile now. Not sure about the part to determine IDs.

b741422

cyrus- reviewed Apr 16, 2024

View reviewed changes